r:CRng, a, b:|r|, n:.
((a +r b) r n) = ((r) 0  i < n+1. choose(n;i) r ((a r i) * (b r (n - i))))  |r| 

latex

Definitions

False, A, A  B, P  Q, t  T, x:A. B(x), P & Q, , x. t(x), P  Q, P  Q, x f y, {i...j}, True, T, , P  Q, tt, if b then t else f fi , Y, choose(n;i), ff, Rng, CRng, i  j < k, x(s), {i..j}, Unit, ,

Lemmas

le wf, crng wf, rng car wf, nat wf, int seg wf, rng nexp wf, rng times wf, choose wf, rng nat op wf, rng sum unroll unit, rng plus wf, rng nexp zero, rng wf, true wf, squash wf, rng one wf, not functionality wrt iff, assert of bnot, and functionality wrt iff, assert of band, bnot thru bor, eqff to assert, not wf, bnot wf, band wf, assert of eq int, or functionality wrt iff, assert of bor, eqtt to assert, assert wf, iff transitivity, bool wf, eq int wf, bor wf, rng nat op one, rng times one, int iseg wf, rng sum wf, rng sum unroll lo, rng sum unroll hi, rng sum plus, rng nat op add, rng nexp unroll, rng plus ac 1, rng plus comm, rng plus assoc, rng times over plus, rng sum shift, rng times sum r, crng times comm, crng times ac 1, rng times assoc, rng times nat op r